Nuprl Definition : R-base-domain
11,40
postcript
pdf
R-base-domain(
R
)
== es_realizer_ind(
R
;
== es_realizer_ind(
<0,
>;
== es_realizer_ind(
left
,
right
,
rec1
,
rec2
.<0,
>;
== es_realizer_ind(
loc
,
T
,
x
,
v
.<1,
x
>;
== es_realizer_ind(
loc
,
T
,
x
,
L
.<2,
x
>;
== es_realizer_ind(
lnk
,
tag
,
L
.<3,
lnk
,
tag
>;
== es_realizer_ind(
loc
,
ds
,
knd
,
T
,
x
,
f
.<4,
knd
,
x
>;
== es_realizer_ind(
ds
,
knd
,
T
,
l
,
dt
,
g
.<5,
knd
,
l
>;
== es_realizer_ind(
loc
,
ds
,
a
,
T
,
P
.<6,
a
>;
== es_realizer_ind(
loc
,
k
,
L
.<7,
k
>;
== es_realizer_ind(
loc
,
k
,
L
.<8,
k
>;
== es_realizer_ind(
loc
,
x
,
L
.<9,
x
>)
latex
Definitions
,
<
a
,
b
>
,
#$n
FDL editor aliases
R-base-domain
origin